\begin{tabbing}
weakPrecondSendR\{\$a,\$tg\}($T$;$p$;$l$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=Rpre(source($l$);${\it ds}$;"\$a";$p$;$P$); \+
\\[0ex]
\\[0ex]Rsends(${\it ds}$;locl("\$a");p{-}outcome($p$);$l$;"\$tg" : $T$;[\=$<$"\$tg", $\lambda$$s$,$v$. [($f$($s$,$v$)) / []]$>$ / \+
\\[0ex][]]) / 
\-\\[0ex][Rsframe($l$;"\$tg";[locl("\$a") / []]) / []]])
\-
\end{tabbing}